﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace OpSatPlan.Encoder
{
    public class ClauseTemplate
    {
        private CnfEncoder mEncoder;
        private Dictionary<VariableTemplate, VariableTemplate> mTemplates;
        public ClauseTemplate(CnfEncoder encoder)
        {
            this.mEncoder = encoder;
            this.mTemplates = new  Dictionary<VariableTemplate, VariableTemplate>();
        }
        public ClauseTemplate(ClauseTemplate copy)
        {
            this.mEncoder = copy.mEncoder;
            this.mTemplates = new  Dictionary<VariableTemplate, VariableTemplate>(copy.mTemplates);
        }
        public void Add(Operator op, bool value)
        {
			VariableTemplate v = new OperatorTemplate(this.mEncoder, op, value);
			if(!this.mTemplates.ContainsKey(v))
            	this.mTemplates.Add(v, v);
        }
        public void Add(AtomicFormula af, int offset, bool value)
        {
			VariableTemplate v = new AtomicFormulaTemplate(this.mEncoder, af, offset, value);
			if(!this.mTemplates.ContainsKey(v))
            	this.mTemplates.Add(v, v);
        }
        public string GenerateClause(int timeStep)
        {
            StringBuilder sb = new StringBuilder(this.mTemplates.Count * 2 + 1);
            foreach (VariableTemplate vt in this.mTemplates.Values)
			{
                sb.Append(vt.GetVariable(timeStep));
				sb.Append(" ");
			}
            sb.Append("0");

            return sb.ToString();
        }
    }
}
